$\forall$${\it es}$:ES, ${\it ff}$:FIFO, ${\it f2f+}$:F2F+{-}decls.
\\[0ex]plus{-}ify\{i:l\}(${\it es}$;${\it ff}$;is\_req  ;is\_ack ;awaiting ;owes\_ack )
\\[0ex]$\Rightarrow$ ($\forall$${\it sndr}$, ${\it rcvr}$:${\it ff}$.C, $a$, $b$, $e$:E. (f2f+{-}pred($e$,$a$) \& f2f+{-}pred($e$,$b$)) $\Rightarrow$ ($a$ = $b$))